\begin{tabbing}
$\forall$$A$:MsgA, $b$:Id, $s$, $s_{0}$:$A$.state.
\\[0ex]ma{-}frame{-}compat($A$;$A$)
\\[0ex]$\Rightarrow$ $b$ in dom($A$.pre)
\\[0ex]$\Rightarrow$ (\=$\forall$$v$:$A$.da(locl($b$)).\+
\\[0ex]$A$.pre($b$,$s$,$v$) $\Leftrightarrow$ $A$.pre($b$,$\lambda$$x$.if $A$:locl($b$) may not read $x$$\rightarrow$ $s_{0}$($x$) else $s$($x$) fi,$v$))
\-
\end{tabbing}